In the reset of this library, we develop tactics to break apart
'if test then truecase else falsecase fi ' terms. Since we have sqequality,
on test, it is possible to break apart these terms without generating
well-formedness subgoals on the 'truecase' and 'falsecase' subterms, even if
term is a hypothesis.